Skip to content

Support user-defined predicate call in annotation #22

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Open
coeff-aij wants to merge 15 commits into
base: main
Choose a base branch
from
Open

Support user-defined predicate call in annotation #22

coeff-aij wants to merge 15 commits into from
+124 −2

Conversation

@coeff-aij
Copy link
Collaborator

@coeff-aij coeff-aij commented Jan 12, 2026 •
edited
Loading

This extention allows users to call arbitrary user-defined predicates (e.g., is_double(x, result)) within annotations.
Currently, a dedicated syntax for defining user-defined predicates is not yet supported. Therefore, users must define them using the #![thrust::raw_define()] (introduced in #21 ) attribute for now.

  • Usage
    The predicate is_double() defined using #![thrust::raw_define()] can be called in the annotations such as #[thrust::ensures()]:
#![feature(custom_inner_attributes)]
#![thrust::raw_define("(define-fun is_double ((x Int) (doubled_x Int)) Bool
    (=
        (* x 2)
        doubled_x
    )
)")]

#[thrust::requires(true)]
#[thrust::ensures(is_double(x, result))]
fn double(x: i64) -> i64 {
    x + x
}

@coeff-aij coeff-aij mentioned this pull request Jan 12, 2026
Closed
@coeff-aij coeff-aij marked this pull request as ready for review January 12, 2026 11:10
@coord-e coord-e self-requested a review January 13, 2026 14:13
coord-e
coord-e reviewed Jan 13, 2026
View reviewed changes
src/chc.rs Outdated
}

#[derive(Debug, Clone, PartialEq, Eq, Hash)]
pub struct UserDefinedPred {
Copy link
Owner

@coord-e coord-e Jan 13, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This struct seems to be unused. I think it's more natural to rename UserDefinedPredSymbol to UserDefinedPred and remove this one.

Copy link
Collaborator Author

@coeff-aij coeff-aij Jan 14, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Originally I defined this struct to implement a parser for definitions of user-defined predicates. If the parser is implemented in the future, it might be fine to leave this definition as is.

Copy link
Owner

@coord-e coord-e Jan 14, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I’d like to avoid leaving unused structs because it makes the intent harder to understand later. Requirements might change by the time we write the parser for the definitions, so I don’t think there's a need to define them speculatively right now. (Either way, I think cargo clippy or something will probably flag it.)

@coeff-aij
Copy link
Collaborator Author

coeff-aij commented Jan 14, 2026

I reflected the comments in above review.

coord-e
coord-e reviewed Jan 20, 2026
View reviewed changes
Copy link
Owner

@coord-e coord-e left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

mostly LGTM, please rebase after merging #21

src/chc.rs
Pred::Matcher(p)
}
}

Copy link
Owner

@coord-e coord-e Jan 20, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

please add impl From<UserDefinedPred> for Pred

Copy link
Collaborator Author

@coeff-aij coeff-aij Jan 20, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I added it.

coord-e
coord-e approved these changes Jan 20, 2026
View reviewed changes
Copy link
Owner

@coord-e coord-e left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you!

@coeff-aij
Copy link
Collaborator Author

coeff-aij commented Jan 20, 2026

I accidentally deleted the tests in git rebase. I have restored them.
Is it okay to squash-merge this PR?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@coord-e coord-e coord-e approved these changes

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@coeff-aij @coord-e